| Definitions | s = t, x:A  B(x), Id, M.(timed)state, if b then t else f fi , (i = j),  x.A(x), M.init(x)?v, M(i), t.1, f(a), n - m, #$n,  , M.state, M.da(a), locl(a), left + right, Unit, IdLnk, M.dout2(l;tg), source(l), M.din(l,tg), destination(l), Dsys, d-comp(D; v; sched; dec; d), Type, {i..j },  , {x:A| B(x)} , d-world-state(D;i),  x:A. B(x), P   Q, t  T, P  Q, P & Q, x:A  B(x),   b,  ,  , A,  b, timedState(ds), Top, f(x)?z, False, A  B, M.ds(x), S  T,  , suptype(S; T), Void, n+m, -n, i j < k, a < b, let x = a in b(x), hd(l), World, d-partial-world(D;f;t';s;d), Action(dec), kindcase(k; a.f(a); l,t.g(l;t) ), a = b, case b of inl(x) => s(x) | inr(y) => t(y), p  q, i = j, i <z j, ||as||, rcv(l,tg), mtag(m), mval(m), queue(l;t), isl(x), doact(k;v), inr x , outl(x), w-knum(w;i;k;t), read-state(s), null, islocal(k), act(k), lnk(k), tag(k), P Q, p  q,  T, True, P Q, Knd, outr(x), t.2, Msg, i  j , SQType(T), {T}, s ~ t, Msg(M), mlnk(m), <a, b>, MsgA, w.M, M.dout(l,tg),  x. t(x), type List, [], filter(P;l), M.sends(k,s,v), M.Msg, Msg(da), M.ef(k,x,s,v)?w, shift-state(s), d-decl(D;i), w-action-dec(TA;M;i), x,y. t(x;y), Atom$n, inl x |
| Lemmas | nat properties, kindcase wf, action wf, d-decl wf, shift-state wf, ma-ef-val wf, mlnk wf d, subtype rel list, filter type, ma-msg wf, ma-send-val wf, mlnk wf, Msg wf, read-state wf, w-knum wf, pi2 wf, pi1 wf, null-action wf, assert-d-eq-Loc, msga wf, true wf, squash wf, mlnk-hd-w-queue, assert-eq-id, hd wf, rcv wf, Knd wf, eq id wf, ifthenelse wf, doact wf, assert of le int, or functionality wrt iff, assert of bor, bnot of lt int, bor wf, bnot thru band, assert of lt int, and functionality wrt iff, assert of band, world wf, d-partial-world wf, le wf, ma-init-val wf, rationals wf, assert wf, not wf, bnot wf, eq int wf, assert of eq int, not functionality wrt iff, assert of bnot, iff transitivity, eqff to assert, eqtt to assert, d-world-state wf, int seg wf, nat wf, dsys wf, ldst wf, d-m wf, ma-din wf, lsrc wf, ma-dout2 wf, Id wf, IdLnk wf, ma-tst wf, unit wf, locl wf, ma-da wf, ma-st wf, bool wf |
